| 1: | from(X) | → cons(X,n__from(n__s(X))) | |
| 2: | length(n__nil) | → 0 | |
| 3: | length(n__cons(X,Y)) | → s(length1(activate(Y))) | |
| 4: | length1(X) | → length(activate(X)) | |
| 5: | from(X) | → n__from(X) | |
| 6: | s(X) | → n__s(X) | |
| 7: | nil | → n__nil | |
| 8: | cons(X1,X2) | → n__cons(X1,X2) | |
| 9: | activate(n__from(X)) | → from(activate(X)) | |
| 10: | activate(n__s(X)) | → s(activate(X)) | |
| 11: | activate(n__nil) | → nil | |
| 12: | activate(n__cons(X1,X2)) | → cons(activate(X1),X2) | |
| 13: | activate(X) | → X | |
| 14: | FROM(X) | → CONS(X,n__from(n__s(X))) | |
| 15: | LENGTH(n__cons(X,Y)) | → S(length1(activate(Y))) | |
| 16: | LENGTH(n__cons(X,Y)) | → LENGTH1(activate(Y)) | |
| 17: | LENGTH(n__cons(X,Y)) | → ACTIVATE(Y) | |
| 18: | LENGTH1(X) | → LENGTH(activate(X)) | |
| 19: | LENGTH1(X) | → ACTIVATE(X) | |
| 20: | ACTIVATE(n__from(X)) | → FROM(activate(X)) | |
| 21: | ACTIVATE(n__from(X)) | → ACTIVATE(X) | |
| 22: | ACTIVATE(n__s(X)) | → S(activate(X)) | |
| 23: | ACTIVATE(n__s(X)) | → ACTIVATE(X) | |
| 24: | ACTIVATE(n__nil) | → NIL | |
| 25: | ACTIVATE(n__cons(X1,X2)) | → CONS(activate(X1),X2) | |
| 26: | ACTIVATE(n__cons(X1,X2)) | → ACTIVATE(X1) | |